Step of Proof: p-fun-exp-add-sq
11,40
postcript
pdf
Inference at
*
2
2
1
2
2
I
of proof for Lemma
p-fun-exp-add-sq
:
.....falsecase..... NILNIL
1.
A
: Type
2.
f
:
A
(
A
+ Top)
3.
x
:
A
4.
m
:
5. 0 <
m
6.
n
:
. (
can-apply(
f
^
m
- 1;
x
))
((
f
^
n
+(
m
- 1)(
x
)) ~ (
f
^
n
(do-apply(
f
^
m
- 1;
x
))))
7.
n
:
8.
can-apply(
f
^
m
;
x
)
9.
(
n
= 0)
10.
(
n
+
m
= 0)
11.
(
n
= 0)
12.
(
m
= 0)
13.
(
can-apply(
f
^
m
- 1;
x
))
(
f
o
f
^
n
(do-apply(
f
^
m
- 1;
x
))) ~ (
f
o
f
^
n
- 1 (outl(
f
^
m
- 1(
x
))))
latex
by (D (-1)
)
CollapseTHEN ((Using [`n',
m
] (BLemma `can-apply-fun-exp`) )
CollapseTHEN (Auto
)
C
)
latex
C
.
Definitions
A
,
False
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
can-apply-fun-exp
origin